A, B, T:Type, x:Id, a:Knd, tg:Id, l:IdLnk, f:(AB(T List)).
(a = rcv(l,tg)  T = B)  a(v) sends [tg,   f(x, v)] on link l    MsgA 

latex

Definitions	Unit, True, P  Q, SQType(T), {T}, P  Q, P & Q, x  dom(f), , b, b, A, False, Id, t  T, a:A fp B(a), Knd, x : v, MsgA, Prop, IdLnk, a(v) sends [tg,   f(x, v)] on link l  , with declarations ds:dsda:dak(v) sends f s v on link l, S  T, IdDeq, State(ds), f(x)?z, f  g, KindDeq, Valtype(da;k), P  Q, x. t(x), rcv(l,tg), x:A. B(x), Top
Lemmas	fpf-cap-single1, fpf-single wf, top wf, fpf-join-cap-sq, rcv wf, fpf-cap wf, ma-valtype wf, ma-state wf, id-deq wf, Kind-deq wf, fpf-join wf, ma-single-sends wf, Knd wf, Id wf, IdLnk wf, assert wf, not wf, bnot wf, bool wf, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, bool sq, eqtt to assert, bool cases, eqof eq btrue, fpf-single-dom